\begin{tabbing}
$\forall$$l$:IdLnk, $p$:(IdLnk List).
\\[0ex]lpath([$l$ / $p$])
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(lpath($p$)\+
\\[0ex]\& (\=($\neg$($\parallel$$p$$\parallel$ = 0))\+
\\[0ex]$\Rightarrow$ (destination($l$) = source(hd($p$)) $\in$ Id \& ($\neg$(hd($p$) = lnk{-}inv($l$) $\in$ IdLnk)))))
\-\-
\end{tabbing}